1  /-
  2  Copyright (c) 2019 Scott Morrison. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Scott Morrison
  5  -/
  6  import topology.sheaves.presheaf
src         └───────────────────────┘
  7  
  8  /-!
  9  # Presheafed spaces
 10  
 11  Introduces the category of topological spaces equipped with a presheaf (taking values in an
 12  arbitrary target category `C`.)
 13  
 14  We further describe how to apply functors and natural transformations to the values of the
 15  presheaves.
 16  -/
 17  
 18  universes v u
 19  
 20  open category_theory
 21  open Top
 22  open topological_space
 23  open opposite
 24  open category_theory.category category_theory.functor
 25  
 26  variables (C : Type u) [𝒞 : category.{v} C]
id                  └──┘         └──────┘
src                              └──────┘
typ                 └──┘         └──────┘
doc                              └──────┘
 27  include 𝒞
 28  
 29  local attribute [tidy] tactic.op_induction'
id                          └──────────────────┘
src                         └──────────────────┘
typ                         └──────────────────┘
doc                   └──┘
 30  
 31  namespace algebraic_geometry
 32  
 33  /-- A `PresheafedSpace C` is a topological space equipped with a presheaf of `C`s. -/
 34  structure PresheafedSpace :=
 35  (to_Top : Top.{v})
id             └─┘
src            └─┘
typ            └─┘
doc            └─┘
 36  (𝒪 : to_Top.presheaf C)
id        └────┘└───────┘ 
src             └───────┘
typ       └────┘└───────┘ 
 37  
 38  variables {C}
 39  
 40  namespace PresheafedSpace
 41  
 42  instance coe_to_Top : has_coe (PresheafedSpace.{v} C) Top :=
id                         └─────┘  └─────────────┘       └─┘
src                        └─────┘  └─────────────┘        └─┘
typ                        └─────┘  └─────────────┘       └─┘
doc                                 └─────────────┘        └─┘
 43  { coe := λ X, X.to_Top }
id                └─────┘
src                 └─────┘
typ               └─────┘
 44  
 45  @[simp] lemma as_coe (X : PresheafedSpace.{v} C) : X.to_Top = (X : Top.{v}) := rfl
id                             └─────────────┘         └─────┘      └─┘         └─┘
src                            └─────────────┘           └─────┘       └─┘         └─┘
typ                            └─────────────┘         └─────┘      └─┘         └─┘
doc    └──┘                    └─────────────┘                          └─┘
 46  @[simp] lemma mk_coe (to_Top) (𝒪) : (({ to_Top := to_Top, 𝒪 := 𝒪 } :
id                                                     └────┘       
typ                                                    └────┘       
doc    └──┘
 47    PresheafedSpace.{v} C) : Top.{v}) = to_Top := rfl
id     └─────────────┘         └─┘       └────┘    └─┘
src    └─────────────┘          └─┘                 └─┘
typ    └─────────────┘         └─┘       └────┘    └─┘
doc    └─────────────┘          └─┘
 48  
 49  instance (X : PresheafedSpace.{v} C) : topological_space X := X.to_Top.str
id                 └─────────────┘         └───────────────┘     └─────┘└──┘
src                └─────────────┘          └───────────────┘       └─────┘└──┘
typ                └─────────────┘         └───────────────┘     └─────┘└──┘
doc                └─────────────┘          └───────────────┘
 50  
 51  /-- A morphism between presheafed spaces `X` and `Y` consists of a continuous map
 52      `f` between the underlying topological spaces, and a (notice contravariant!) map
 53      from the presheaf on `Y` to the pushforward of the presheaf on `X` via `f`. -/
 54  structure hom (X Y : PresheafedSpace.{v} C) :=
id                        └─────────────┘     
src                       └─────────────┘
typ                       └─────────────┘     
doc                       └─────────────┘
 55  (f : (X : Top.{v}) ⟶ (Y : Top.{v}))
id            └─┘           └─┘
src            └─┘            └─┘
typ           └─┘           └─┘
doc            └─┘             └─┘
 56  (c : Y.𝒪 ⟶ f _* X.𝒪)
id        └┘   └┘ └┘
src        └┘    └┘  └┘
typ       └┘   └┘ └┘
 57  
 58  @[ext] lemma ext {X Y : PresheafedSpace.{v} C} (α β : hom X Y)
id                           └─────────────┘              └─┘  
src                          └─────────────┘               └─┘
typ                          └─────────────┘              └─┘  
doc    └─┘                   └─────────────┘               └─┘
 59    (w : α.f = β.f) (h : α.c ≫ (whisker_right (nat_trans.op (opens.map_iso _ _ w).inv) X.𝒪) = β.c) :
id          └┘  └┘       └┘   └───────────┘  └──────────┘  └───────────┘      └─┘   └┘   └┘
src          └┘   └┘        └┘   └───────────┘  └──────────┘  └───────────┘       └─┘    └┘    └┘
typ         └┘  └┘       └┘   └───────────┘  └──────────┘  └───────────┘      └─┘   └┘   └┘
 60    α = β :=
id       
src      
typ      
 61  begin
st   └─────
 62    cases α, cases β,
id                   
src    └────┘   └────┘
typ    └────┘  └────┘
doc    └────┘   └────┘
txt    └────┘   └────┘
par    └────┘   └────┘
pid                 
st   ────────┘└───────┘└─
 63    dsimp [presheaf.pushforward] at *,
id            └──────────────────┘
src    └─────┘└──────────────────┘└────┘
typ    └─────┘└──────────────────┘└────┘
doc    └─────┘                    └────┘
txt    └─────┘                    └────┘
par    └─────┘                    └────┘
pid                             └──┘
st   ──────────────────────────────────┘└─
 64    tidy, -- TODO including `injections` would make tidy work earlier.
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└──────────────────────────────────────────────────────────────
 65  end
st   ──┘
 66  .
 67  
 68  def id (X : PresheafedSpace.{v} C) : hom X X :=
id               └─────────────┘         └─┘  
src              └─────────────┘          └─┘
typ              └─────────────┘         └─┘  
doc              └─────────────┘          └─┘
 69  { f := 𝟙 (X : Top.{v}),
id               └─┘
src               └─┘
typ              └─┘
doc                └─┘
 70    c := ((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id (X.to_Top)).hom) _) }
id            └─────────────────┘   └─┘     └───────────┘  └──────────┘  └──────────┘  └─────┘  └─┘
src           └─────────────────┘   └─┘     └───────────┘  └──────────┘  └──────────┘   └─────┘  └─┘
typ           └─────────────────┘   └─┘     └───────────┘  └──────────┘  └──────────┘  └─────┘  └─┘
 71  
 72  def comp (X Y Z : PresheafedSpace.{v} C) (α : hom X Y) (β : hom Y Z) : hom X Z :=
id                     └─────────────┘            └─┘         └─┘      └─┘  
src                    └─────────────┘             └─┘           └─┘        └─┘
typ                    └─────────────┘            └─┘         └─┘      └─┘  
doc                    └─────────────┘             └─┘           └─┘        └─┘
 73  { f := α.f ≫ β.f,
id          └┘  └┘
src          └┘   └┘
typ         └┘  └┘
 74    c := β.c ≫ (whisker_left (opens.map β.f).op α.c) }
id          └┘   └──────────┘  └───────┘ └┘ └┘  └┘
src          └┘   └──────────┘  └───────┘  └┘ └┘   └┘
typ         └┘   └──────────┘  └───────┘ └┘ └┘  └┘
doc                              └───────┘
 75  
 76  variables (C)
 77  
 78  section
 79  local attribute [simp] id comp presheaf.pushforward
id                          └┘ └──┘ └──────────────────┘
src                         └┘ └──┘ └──────────────────┘
typ                         └┘ └──┘ └──────────────────┘
doc                   └──┘
 80  
 81  /- The proofs below can be done by `tidy`, but it is too slow,
 82     and we don't have a tactic caching mechanism. -/
 83  /-- The category of PresheafedSpaces. Morphisms are pairs, a continuous map and a presheaf map
 84      from the presheaf on the target to the pushforward of the presheaf on the source. -/
 85  instance category_of_PresheafedSpaces : category (PresheafedSpace.{v} C) :=
id                                           └──────┘  └─────────────┘     
src                                          └──────┘  └─────────────┘
typ                                          └──────┘  └─────────────┘     
doc                                          └──────┘  └─────────────┘
 86  { hom := hom,
id            └─┘
src           └─┘
typ           └─┘
doc           └─┘
 87    id := id,
id           └┘
src          └┘
typ          └┘
 88    comp := comp,
id             └──┘
src            └──┘
typ            └──┘
 89    id_comp' := λ X Y f,
id                     
typ                    
 90    begin
st     └─────
 91      ext1, swap,
src      └──┘  └──┘
typ      └──┘  └──┘
doc      └──┘  └──┘
txt      └──┘  └──┘
par      └──┘  └──┘
st   ───────┘└────┘└─
 92      { dsimp, simp only [id_comp] },
id                           └─────┘
src        └───┘  └─────────┘└─────┘└┘
typ        └───┘  └─────────┘└─────┘└┘
doc        └───┘  └─────────┘       └┘
txt        └───┘  └─────────┘       └┘
par        └───┘  └─────────┘       └┘
pid                   └──┘└┘       
st   ─────┘└───┘└────────────────────┘└┘
 93      { ext U,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid           └┘
st   ──────────┘└─
 94        op_induction,
src        └──────────┘
typ        └──────────┘
txt        └──────────┘
par        └──────────┘
st   ─────────────────┘└─
 95        cases U,
id               
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────┘└─
 96        dsimp,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
 97        simp only [comp_id, map_id] },
id                    └─────┘  └────┘
src        └─────────┘└─────┘└┘└────┘└┘
typ        └─────────┘└─────┘└┘└────┘└┘
doc        └─────────┘       └┘      └┘
txt        └─────────┘       └┘      └┘
par        └─────────┘       └┘      └┘
pid            └──┘└┘       └┘      
st   ─────────────────────────────────┘└──
 98    end,
st   ────┘
 99    comp_id' := λ X Y f,
id                     
typ                    
100    begin
st     └─────
101      ext1, swap,
src      └──┘  └──┘
typ      └──┘  └──┘
doc      └──┘  └──┘
txt      └──┘  └──┘
par      └──┘  └──┘
st   ───────┘└────┘└─
102      { dsimp, simp only [comp_id] },
id                           └─────┘
src        └───┘  └─────────┘└─────┘└┘
typ        └───┘  └─────────┘└─────┘└┘
doc        └───┘  └─────────┘       └┘
txt        └───┘  └─────────┘       └┘
par        └───┘  └─────────┘       └┘
pid                   └──┘└┘       
st   ─────┘└───┘└────────────────────┘└┘
103      { ext U,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid           └┘
st   ──────────┘└─
104        op_induction,
src        └──────────┘
typ        └──────────┘
txt        └──────────┘
par        └──────────┘
st   ─────────────────┘└─
105        cases U,
id               
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────┘└─
106        dsimp,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
107        simp only [comp_id, id_comp, map_id] }
id                    └─────┘  └─────┘  └────┘
src        └─────────┘└─────┘└┘└─────┘└┘└────┘└┘
typ        └─────────┘└─────┘└┘└─────┘└┘└────┘└┘
doc        └─────────┘       └┘       └┘      └┘
txt        └─────────┘       └┘       └┘      └┘
par        └─────────┘       └┘       └┘      └┘
pid            └──┘└┘       └┘       └┘      
st   ──────────────────────────────────────────┘└─
108    end,
st   ────┘
109    assoc' := λ W X Y Z f g h,
id                       
typ                      
110    begin
st     └─────
111      simp only [true_and, presheaf.pushforward, id, comp, whisker_left_twice, whisker_left_comp,
id                  └──────┘  └──────────────────┘  └┘  └──┘  └────────────────┘  └───────────────┘
src      └─────────┘└──────┘└┘└──────────────────┘└┘└┘└┘└──┘└┘└────────────────┘└┘└───────────────┘└─
typ      └─────────┘└──────┘└┘└──────────────────┘└┘└┘└┘└──┘└┘└────────────────┘└┘└───────────────┘└─
doc      └─────────┘        └┘                    └┘  └┘    └┘                  └┘                 └─
txt      └─────────┘        └┘                    └┘  └┘    └┘                  └┘                 └─
par      └─────────┘        └┘                    └┘  └┘    └┘                  └┘                 └─
pid          └──┘└┘        └┘                    └┘  └┘    └┘                  └┘                 └─
st   ────────────────────────────────────────────────────────────────────────────────────────────────
112                 heq_iff_eq, category.assoc],
id                  └────────┘  └────────────┘
src  ──────────────┘└────────┘└┘└────────────┘
typ  ──────────────┘└────────┘└┘└────────────┘
doc  ──────────────┘          └┘              
txt  ──────────────┘          └┘              
par  ──────────────┘          └┘              
pid  ──────────────┘          └┘              
st   ─────────────────────────────────────────┘└─
113      split; refl
src      └───┘  └────
typ      └───┘  └────
doc      └───┘  └────
txt      └───┘  └────
par      └───┘  └────
pid                 
st   ────────────────
114    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
115  
116  end
117  
118  variables {C}
119  
120  instance {X Y : PresheafedSpace.{v} C} : has_coe (X ⟶ Y) (X.to_Top ⟶ Y.to_Top) :=
id                   └─────────────┘         └─────┘       └─────┘  └─────┘
src                  └─────────────┘          └─────┘          └─────┘   └─────┘
typ                  └─────────────┘         └─────┘       └─────┘  └─────┘
doc                  └─────────────┘
121  { coe := λ α, α.f }
id                └┘
src                 └┘
typ               └┘
122  
123  @[simp] lemma hom_mk_coe {X Y : PresheafedSpace.{v} C} (f) (c) :
id                                   └─────────────┘     
src                                  └─────────────┘
typ                                  └─────────────┘     
doc    └──┘                          └─────────────┘
124    (({ f := f, c := c } : X ⟶ Y) : (X : Top.{v}) ⟶ (Y : Top.{v})) = f := rfl
id                                    └─┘           └─┘            └─┘
src                                        └─┘            └─┘             └─┘
typ                                   └─┘           └─┘            └─┘
doc                                         └─┘             └─┘
125  @[simp] lemma f_as_coe {X Y : PresheafedSpace.{v} C} (α : X ⟶ Y) :
id                                 └─────────────┘              
src                                └─────────────┘               
typ                                └─────────────┘              
doc    └──┘                        └─────────────┘
126    α.f = (α : (X : Top.{v}) ⟶ (Y : Top.{v})) := rfl
id     └┘          └─┘           └─┘          └─┘
src     └┘            └─┘            └─┘          └─┘
typ    └┘          └─┘           └─┘          └─┘
doc                    └─┘             └─┘
127  @[simp] lemma id_coe (X : PresheafedSpace.{v} C) :
id                             └─────────────┘     
src                            └─────────────┘
typ                            └─────────────┘     
doc    └──┘                    └─────────────┘
128    (((𝟙 X) : X ⟶ X) : (X : Top.{v}) ⟶ X) = 𝟙 (X : Top.{v}) := rfl
id                       └─┘               └─┘         └─┘
src                          └─┘                 └─┘         └─┘
typ                      └─┘               └─┘         └─┘
doc                            └─┘                    └─┘
129  @[simp] lemma comp_coe {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
id                                   └─────────────┘                       
src                                  └─────────────┘                          
typ                                  └─────────────┘                       
doc    └──┘                          └─────────────┘
130    ((α ≫ β : X ⟶ Z) : (X : Top.{v}) ⟶ Z) = (α : (X : Top.{v}) ⟶ Y) ≫ (β : Y ⟶ Z) := rfl
id                      └─┘                  └─┘                     └─┘
src                          └─┘                     └─┘                         └─┘
typ                     └─┘                  └─┘                     └─┘
doc                            └─┘                       └─┘
131  
132  lemma id_c (X : PresheafedSpace.{v} C) :
id                   └─────────────┘     
src                  └─────────────┘
typ                  └─────────────┘     
doc                  └─────────────┘
133    ((𝟙 X) : X ⟶ X).c =
id                 
src                   
typ                
134    (((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id (X.to_Top)).hom) _)) := rfl
id        └─────────────────┘   └─┘     └───────────┘  └──────────┘  └──────────┘  └─────┘  └─┘          └─┘
src       └─────────────────┘   └─┘     └───────────┘  └──────────┘  └──────────┘   └─────┘  └─┘          └─┘
typ       └─────────────────┘   └─┘     └───────────┘  └──────────┘  └──────────┘  └─────┘  └─┘          └─┘
135  
136  -- Implementation note: this harmless looking lemma causes deterministic timeouts,
137  -- but happily we can survive without it.
138  -- lemma comp_c {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
139  --   (α ≫ β).c = (β.c ≫ (whisker_left (opens.map β.f).op α.c)) := rfl
140  
141  @[simp] lemma id_c_app (X : PresheafedSpace.{v} C) (U) :
id                               └─────────────┘     
src                              └─────────────┘
typ                              └─────────────┘     
doc    └──┘                      └─────────────┘
142    ((𝟙 X) : X ⟶ X).c.app U = eq_to_hom (by { op_induction U, cases U, refl }) :=
id                └─┘    └───────┘                             
src                  └─┘     └───────┘       └────────────┘  └────┘   └───┘
typ               └─┘    └───────┘       └────────────┘  └────┘  └───┘
doc                                                              └────┘   └───┘
txt                                              └────────────┘  └────┘   └───┘
par                                              └────────────┘  └────┘   └───┘
pid                                                          └┘              
st                                            └───────────────┘└───────┘└─────┘└┘
143  by { op_induction U, cases U, simp only [id_c], dsimp, simp, }
id                                           └──┘
src       └────────────┘  └────┘   └─────────┘└──┘  └───┘  └──┘
typ       └────────────┘  └────┘  └─────────┘└──┘  └───┘  └──┘
doc                       └────┘   └─────────┘      └───┘  └──┘
txt       └────────────┘  └────┘   └─────────┘      └───┘  └──┘
par       └────────────┘  └────┘   └─────────┘      └───┘  └──┘
pid                   └┘              └──┘└┘    
st     └───────────────┘└───────┘└────────────────┘└─────┘└────┘└──┘
144  
145  @[simp] lemma comp_c_app {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
id                                     └─────────────┘                       
src                                    └─────────────┘                          
typ                                    └─────────────┘                       
doc    └──┘                            └─────────────┘
146    (α ≫ β).c.app U = (β.c).app U ≫ (α.c).app (op ((opens.map (β.f)).obj (unop U))) := rfl
id          └─┘     └┘ └─┘     └┘ └─┘   └┘   └───────┘  └┘  └─┘   └──┘        └─┘
src           └─┘       └┘ └─┘       └┘ └─┘   └┘   └───────┘   └┘  └─┘   └──┘         └─┘
typ         └─┘     └┘ └─┘     └┘ └─┘   └┘   └───────┘  └┘  └─┘   └──┘        └─┘
doc                                                    └───────┘
147  
148  /-- The forgetful functor from `PresheafedSpace` to `Top`. -/
149  def forget : PresheafedSpace.{v} C ⥤ Top :=
id                └─────────────┘       └─┘
src               └─────────────┘        └─┘
typ               └─────────────┘       └─┘
doc               └─────────────┘        └─┘
150  { obj := λ X, (X : Top.{v}),
id                   └─┘
src                    └─┘
typ                  └─┘
doc                    └─┘
151    map := λ X Y f, f }
id                  
typ                 
152  
153  end PresheafedSpace
154  
155  end algebraic_geometry
156  
157  open algebraic_geometry algebraic_geometry.PresheafedSpace
158  
159  variables {C}
160  
161  namespace category_theory
162  
163  variables {D : Type u} [𝒟 : category.{v} D]
id                               └──────┘
src                              └──────┘
typ                              └──────┘
doc                              └──────┘
164  include 𝒟
165  
166  local attribute [simp] presheaf.pushforward
id                          └──────────────────┘
src                         └──────────────────┘
typ                         └──────────────────┘
doc                   └──┘
167  
168  namespace functor
169  
170  /-- We can apply a functor `F : C ⥤ D` to the values of the presheaf in any `PresheafedSpace C`,
171      giving a functor `PresheafedSpace C ⥤ PresheafedSpace D` -/
172  /- The proofs below can be done by `tidy`, but it is too slow,
173     and we don't have a tactic caching mechanism. -/
174  def map_presheaf (F : C ⥤ D) : PresheafedSpace.{v} C ⥤ PresheafedSpace.{v} D :=
id                               └─────────────┘       └─────────────┘     
src                                └─────────────┘        └─────────────┘
typ                              └─────────────┘       └─────────────┘     
doc                                └─────────────┘        └─────────────┘
175  { obj := λ X, { to_Top := X.to_Top, 𝒪 := X.𝒪 ⋙ F },
id                            └─────┘       └┘  
src                             └─────┘        └┘ 
typ                           └─────┘       └┘  
doc                                               
176    map := λ X Y f, { f := f.f, c := whisker_right f.c F },
id                         └┘       └───────────┘ └┘ 
src                            └┘       └───────────┘  └┘
typ                        └┘       └───────────┘ └┘ 
177    map_id' := λ X,
id                  
typ                 
178    begin
st     └─────
179      ext1, swap,
src      └──┘  └──┘
typ      └──┘  └──┘
doc      └──┘  └──┘
txt      └──┘  └──┘
par      └──┘  └──┘
st   ───────┘└────┘└─
180      { refl },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ─────┘└───┘└┘
181      { ext,
src        └─┘
typ        └─┘
doc        └─┘
txt        └─┘
par        └─┘
st   ────────┘└─
182        dsimp,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
183        simp only [presheaf.pushforward, eq_to_hom_map, map_id, comp_id, id_c_app],
id                    └──────────────────┘  └───────────┘  └────┘  └─────┘  └──────┘
src        └─────────┘└──────────────────┘└┘└───────────┘└┘└────┘└┘└─────┘└┘└──────┘
typ        └─────────┘└──────────────────┘└┘└───────────┘└┘└────┘└┘└─────┘└┘└──────┘
doc        └─────────┘                    └┘             └┘      └┘       └┘        
txt        └─────────┘                    └┘             └┘      └┘       └┘        
par        └─────────┘                    └┘             └┘      └┘       └┘        
pid            └──┘└┘                    └┘             └┘      └┘       └┘        
st   ───────────────────────────────────────────────────────────────────────────────┘└─
184        refl }
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└─
185    end,
st   ────┘
186    map_comp' := λ X Y Z f g,
id                        
typ                       
187    begin
st     └─────
188      ext1, swap,
src      └──┘  └──┘
typ      └──┘  └──┘
doc      └──┘  └──┘
txt      └──┘  └──┘
par      └──┘  └──┘
st   ───────┘└────┘└─
189      { refl, },
src        └──┘
typ        └──┘
doc        └──┘
txt        └──┘
par        └──┘
st   ─────┘└──┘└──┘
190      { ext, dsimp, simp only [comp_id, assoc, map_comp, map_id], },
id                                └─────┘  └───┘  └──────┘  └────┘
src        └─┘  └───┘  └─────────┘└─────┘└┘└───┘└┘└──────┘└┘└────┘
typ        └─┘  └───┘  └─────────┘└─────┘└┘└───┘└┘└──────┘└┘└────┘
doc        └─┘  └───┘  └─────────┘       └┘     └┘        └┘      
txt        └─┘  └───┘  └─────────┘       └┘     └┘        └┘      
par        └─┘  └───┘  └─────────┘       └┘     └┘        └┘      
pid                        └──┘└┘       └┘     └┘        └┘      
st   ────────┘└─────┘└────────────────────────────────────────────┘└────
191    end }
st   ────┘
192  
193  @[simp] lemma map_presheaf_obj_X (F : C ⥤ D) (X : PresheafedSpace.{v} C) :
id                                                  └─────────────┘     
src                                                   └─────────────┘
typ                                                 └─────────────┘     
doc    └──┘                                           └─────────────┘
194    ((F.map_presheaf.obj X) : Top.{v}) = (X : Top.{v}) := rfl
id       └───────────┘└──┘     └─┘           └─┘         └─┘
src       └───────────┘└──┘      └─┘            └─┘         └─┘
typ      └───────────┘└──┘     └─┘           └─┘         └─┘
doc       └───────────┘          └─┘             └─┘
195  @[simp] lemma map_presheaf_obj_𝒪 (F : C ⥤ D) (X : PresheafedSpace.{v} C) :
id                                                  └─────────────┘     
src                                                   └─────────────┘
typ                                                 └─────────────┘     
doc    └──┘                                           └─────────────┘
196    (F.map_presheaf.obj X).𝒪 = X.𝒪 ⋙ F := rfl
id      └───────────┘└──┘     └┘      └─┘
src      └───────────┘└──┘       └┘       └─┘
typ     └───────────┘└──┘     └┘      └─┘
doc      └───────────┘                
197  @[simp] lemma map_presheaf_map_f (F : C ⥤ D) {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) :
id                                                    └─────────────┘              
src                                                     └─────────────┘               
typ                                                   └─────────────┘              
doc    └──┘                                             └─────────────┘
198    ((F.map_presheaf.map f) : (X : Top.{v}) ⟶ (Y : Top.{v})) = f := rfl
id       └───────────┘└──┘         └─┘           └─┘            └─┘
src       └───────────┘└──┘           └─┘            └─┘             └─┘
typ      └───────────┘└──┘         └─┘           └─┘            └─┘
doc       └───────────┘               └─┘             └─┘
199  @[simp] lemma map_presheaf_map_c (F : C ⥤ D) {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) :
id                                                    └─────────────┘              
src                                                     └─────────────┘               
typ                                                   └─────────────┘              
doc    └──┘                                             └─────────────┘
200    (F.map_presheaf.map f).c = whisker_right f.c F := rfl
id      └───────────┘└──┘     └───────────┘ └┘     └─┘
src      └───────────┘└──┘      └───────────┘  └┘      └─┘
typ     └───────────┘└──┘     └───────────┘ └┘     └─┘
doc      └───────────┘
201  
202  end functor
203  
204  namespace nat_trans
205  
206  /- The proofs below can be done by `tidy`, but it is too slow,
207     and we don't have a tactic caching mechanism. -/
208  def on_presheaf {F G : C ⥤ D} (α : F ⟶ G) : G.map_presheaf ⟶ F.map_presheaf :=
id                                         └───────────┘  └───────────┘
src                                             └───────────┘   └───────────┘
typ                                        └───────────┘  └───────────┘
doc                                              └───────────┘    └───────────┘
209  { app := λ X,
id              
typ             
210    { f := 𝟙 _,
id            
src           
typ           
211      c := whisker_left X.𝒪 α ≫ ((functor.left_unitor _).inv) ≫
id            └──────────┘ └┘     └─────────────────┘   └─┘   
src           └──────────┘  └┘      └─────────────────┘   └─┘   
typ           └──────────┘ └┘     └─────────────────┘   └─┘   
212             (whisker_right (nat_trans.op (opens.map_id X.to_Top).hom) _) },
id               └───────────┘  └──────────┘  └──────────┘ └─────┘ └─┘
src              └───────────┘  └──────────┘  └──────────┘  └─────┘ └─┘
typ              └───────────┘  └──────────┘  └──────────┘ └─────┘ └─┘
213    naturality' := λ X Y f,
id                        
typ                       
214    begin
st     └─────
215      ext1, swap,
src      └──┘  └──┘
typ      └──┘  └──┘
doc      └──┘  └──┘
txt      └──┘  └──┘
par      └──┘  └──┘
st   ───────┘└────┘└─
216      { refl },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ─────┘└───┘└┘
217      { ext U,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid           └┘
st   ──────────┘└─
218        op_induction,
src        └──────────┘
typ        └──────────┘
txt        └──────────┘
par        └──────────┘
st   ─────────────────┘└─
219        cases U,
id               
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────┘└─
220        dsimp,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
221        simp only [comp_id, assoc, map_id, nat_trans.naturality] }
id                    └─────┘  └───┘  └────┘  └──────────────────┘
src        └─────────┘└─────┘└┘└───┘└┘└────┘└┘└──────────────────┘└┘
typ        └─────────┘└─────┘└┘└───┘└┘└────┘└┘└──────────────────┘└┘
doc        └─────────┘       └┘     └┘      └┘                    └┘
txt        └─────────┘       └┘     └┘      └┘                    └┘
par        └─────────┘       └┘     └┘      └┘                    └┘
pid            └──┘└┘       └┘     └┘      └┘                    
st   ──────────────────────────────────────────────────────────────┘└─
222    end }
st   ────┘
223  
224  -- TODO Assemble the last two constructions into a functor
225  --   `(C ⥤ D) ⥤ (PresheafedSpace C ⥤ PresheafedSpace D)`
226  end nat_trans
227  
228  end category_theory